#pragma once
#include "PDTExpNumSing.h"
#include "PDTConst.h"

class PDTNumConst  :  public PDTExpNumSing, public PDTConst, public TraverseIfc <PDTNumConst , PDTNode> { 
    public: TRAVERSAL_IFC_IMPL(PDTNumConst )
public:
  PDTNumConst(PDTCodeGraph & CG);
  NodeTypeEnum getType() {
    return PDTNumConst_Em;
  }
  virtual PDTNode* getNode() const {
    return (PDTNode*)this;
  }
};

class PDTNumConstInt  :  public PDTNumConst, public TraverseIfc <PDTNumConstInt , PDTNode> { 
    public: TRAVERSAL_IFC_IMPL(PDTNumConstInt )
private:
  long long value;
public:
  PDTNumConstInt(PDTCodeGraph & CG, long long v);

  int getValue()  {
      if (this == NULL) pdt_throw PDTNullValEx;
      return value;
  }

  virtual long long getNumber () const {
      if (this == NULL) pdt_throw PDTNullValEx;
      return value;
  }

  bool isNumConstInt() {
    return true;
  }

  virtual bool isEqual (const PDTConst & rhs) const {
        if (!rhs.getNode()->isNumConstInt())
            return false;
        return value == rhs.getNumber();
  }

  NodeTypeEnum getType() {
    return PDTNumConstInt_Em;
  }

  virtual bool eval(PDTCodeGraph &CG) {
//	  nValue = dynamic_cast<PDTNode*>(this);
	  return true;
  }

	virtual PDTNode* clone(PDTCodeGraph &CG) {
		return this;
	}


  virtual stringstream &
  toString(stringstream & ss) const
  {
    ss << value;
    return ss;
  }

  virtual Z3_ast
  Z3NodeVisit (PDTZ3Visitor &ZV);
};

class PDTNumConstDbl  :  public PDTNumConst, public TraverseIfc <PDTNumConstDbl , PDTNode> { 
    public:  TRAVERSAL_IFC_IMPL(PDTNumConstDbl )
private:
  double value;

public:
  //	void initialize();
  PDTNumConstDbl(PDTCodeGraph & CG, double value);

  virtual double getValue () {
      if (this == NULL) pdt_throw PDTNullValEx;
      return value;
  }

  virtual double getDouble() const {
      if (this == NULL) pdt_throw PDTNullValEx;
      return value;
  }

  NodeTypeEnum
  getType()
  {
    return PDTNumConstDbl_Em;
  }

  bool
  isNumConstDbl()
  {
    return true;
  }
  virtual bool isEqual (const PDTConst & rhs) const {
        if (!rhs.getNode()->isNumConstDbl())
            return false;
        return value == rhs.getDouble();
  }


  virtual bool eval(PDTCodeGraph &CG)
  {
//	  nValue = dynamic_cast<PDTNode*>(this);
	  return true;
  }

	virtual PDTNode* clone(PDTCodeGraph &CG)
	{
		return this;
	}

  virtual stringstream &
  toString(stringstream & ss) const
  {
    ss << value;
    return ss;
  }

  virtual Z3_ast
  Z3NodeVisit (PDTZ3Visitor &ZV);
};
